i:Id, T:Type, v:(T), x:Id.
@i: x:T initially x = v realizes es. (vartype(i;x) r T) c (es_init(es)(i,x) = v) 

latex

Definitions

t  T, x:A. B(x), Id, Action(i), x:AB(x), P  Q, IdLnk, IdDeq, True, b, #$n, A  B, a < b, Void, False, A, , {x:A| B(x)} , , x:A  B(x), P & Q, A c B, {T}, f(x), x  dom(f), mk-ma, x : v, f(x)?z, z != f(x)  P(a;z), x : t initially x = v, M.ds(x), M.bframe(k sends on l), M(i), @i: x:T initially x = v, M.aframe(k affects x), M.sframe(k sends <l,tg>), M.frame(k affects x), M.send(k;l;s;v;ms;i), M.ef(k,x,s,v,w), M.pre(a,s), M.init(x,v), PossibleWorld(D;w), es-T(es), es_init(es), ES(the_w), vartype(i;x), , s = t, FairFifo, World, D realizes2 es.P(es), es_vartype(es;i;x), f(a), es_state(es;i), Type, , x:A. B(x), es is an event system of D, ES, x.A(x), x. t(x), D realizes es. P(es), vartype(i;x)

Lemmas

d-realizes2-implies-realizes, event system wf, d-es wf, es init wf, subtype rel function, es-vartype wf, subtype rel self, rationals wf, world wf, fair-fifo wf, possible-world wf, d-single-init wf, le wf, eqof eq btrue, Id wf, id-deq wf